Declarative Logic Programming
In declarative logic programming, we don't describe how a result is computed. Instead, we specify logical rules that the result has to satisfy, and it is the computer's job to figure out how to compute the result. For example, the set of paths in a graph can be defined recursively as follows:
- If there is an edge from A to B, then there is a path from A to B.
- If there is an edge from A to B and a path from B to C, then there is a path from A to C.
In the logic programming language Datalog, this could be expressed as follows:
path(A, B) :- edge(A, B).
path(A, C) :- edge(A, B), path(B, C).
Note that we just translated our informal description. The result of this program (which is called the fixed point) can be computed by applying the two rules iteratively. In the path program, this means first computing all paths of length one, then two, etc.
In the seminar, you will look at:
- The semantics of Datalog,
- How Datalog programs can be evaluated/compiled efficiently,
- Which applications logic programming is suitable for, and/or
- Which other (functional) approaches to computation of fixed points exist (see References).
You will also write a small program that either
- Uses Datafun or Datalog (see Soufflé and Ascent) to implement a use case (e.g. something on graphs or program analysis), or
- Implements the core of seminaïve evaluation.
In the project, you will implement a compiler for Datalog or a similar language.